 {\em Higher-order process calculi} are calculi 
in which  processes  can be communicated. 
They 
have been put forward in the 
early 1990s,
with 
 CHOCS \cite{Tho89}, Plain CHOCS
\cite{Tho93}, the  Higher-Order $\pi$-calculus 
\cite{San923}, and others. 
Higher-order (or process-passing) concurrency is often presented as an
alternative paradigm 
to the  first order (or name-passing) concurrency of the $\pi$-calculus
for the   description of   mobile systems.    
These calculi are inspired by, and formally closer to the
$\lambda$-calculus, whose basic computational step --- $\beta$-reduction ---
involves term instantiation. As in the $\lambda$-calculus, a computational step in higher-order calculi results in the
instantiation of a variable with a term, which is then
copied as many times as there are occurrences of the variable. 

\hocore is a core calculus for higher-order concurrency, 
recently introduced in \cite{LanesePSS08}.
It is \emph{minimal}, in that only the operators strictly necessary to obtain
 higher-order communications are retained. For instance,
continuations  following  output messages
   have been left out.  More importantly, \hocore has no restriction
   operator.
   Thus all channels are global, and
    dynamic creation of new channels is impossible.
    This makes
    the absence of recursion also relevant, as 
known encodings of fixed-point combinators in 
higher-order  process calculi
require the restriction
operator.
The grammar of \hocore processes is:
\vspace{-2mm}
\[P :: = \inp a x. P \midd \Ho{a}{P} \midd P \parallel P \midd x \midd \nil \qquad \quad (*)\vspace{-2mm}\]  
An  input prefixed process 
$\inp a x . P$ can receive  on
name (or channel) $a$ a process that will be substituted in the place of $x$ in the body $P$;
an output message  $\Ho{a}{P}$ can send $P$ (the output object) on $a$;  parallel composition 
allows processes to interact. 
% \hocore can be seen 
% as  a kind of concurrent
% $\lambda$-calculus, where $\inp a x. P$ is a function, with formal
% parameter $x$ and body $P$, located at  $a$; and
% $\Ho{a}{P}$ is the argument  for such a function.% located at $a$. 

Despite this minimality, via a termination preserving encoding of Minsky machines \cite{Minsky67}, \hocore was shown to be Turing complete. 
Therefore,  in \hocore, properties such as \emph{termination} (i.e. non existence of divergent computations) and 
\emph{convergence} (i.e. existence of a terminating computation)\footnote{Termination and convergence are also referred to as \emph{universal} and \emph{existential} termination, respectively.}  are both undecidable. 
In contrast, somewhat surprisingly, strong bisimilarity is decidable, and 
%Furthermore, 
several sensible bisimilarities in the higher-order setting coincide with it. 


In this paper, we shall aim at identifying the intrinsic source of expressive power in \hocore.
%It can be said that a 
%Our initial observation is that a
A
 substantial part of the expressive power of a concurrent language comes from the ability of accounting for infinite behavior. In higher-order process calculi there is no explicit operator for such a behavior, as both recursion and replication can be encoded. We then find that infinite behavior % is devoted to this aim, this feature 
resides in 
the interplay of higher-order communication, in particular, in 
the ability of %receiving a process and 
\emph{forwarding} 
a received process within
an arbitrary context. % containing a received process.
%More precisely, 
For instance, 
consider the process $R = a(x).\Ho{b}{P_x}$ (here $P_x$ stands for a process $P$ with free occurrences of a variable $x$).  Intuitively, $R$ receives a process on name $a$ and forwards it on name $b$. It is easy to see that since
objects in output actions are 
built following the syntax given by $(*)$, the actual structure of 
$P_x$ can be fairly complex. 
One could even ``wrap'' the process to be received in $x$ using an arbitrary number of $k$ ``output layers'', i.e., by letting
$P_x \equiv \Ho{b_1}{\Ho{b_2}{\ldots \Ho{b_k}{x}}\ldots}$. 
This nesting capability embodies a great deal of the expressiveness of \hocore: as a matter of fact, the encoding of Minsky machines in \cite{LanesePSS08} depends critically on nesting-based counters.
Therefore, investigating suitable limitations to the 
kind of processes that can be communicated in an output action seems a legitimate approach for assessing the expressive power of higher-order concurrency.

With the above consideration in mind, in this paper we propose \ahopi, a sublanguage of \hocore in which output actions 
are limited so as to rule out the nesting capability. In \ahopi, 
output actions can communicate
the parallel composition of
two kinds of objects: (i) statically known closed processes (i.e. that
do not contain free variables), and (ii) processes received
through previously executed input actions.
Hence,
the context in which the output action resides can only contribute to communication by
``appending'' pieces of code that admit no inspection, available in the form of a black-box.
%every output object must be structurally congruent to the parallel composition of two kinds of processes: 
%(i) a number of (possibly open) previously received processes, and 
%(ii) a number of closed processes that available in the local context of the sender. 
%Hence, the context in which the output action resides can only
%contribute to the communication by ``appending'' pieces of code that are available in the form of a black-box.
More formally, the grammar of \ahopi processes is that in $(*)$, excepting the production for output actions, which is replaced by the following one:
\vspace{-2mm}
\[
\Ho{a}{ x_1 \parallel \cdots \parallel x_k \parallel P} \vspace{-2mm}
\]
where $k \geq 0$ and $P$ is a closed process.
This modification directly restricts forwarding capabilities for output processes, which in turn, leads to a more limited structure of processes along reductions.

In addition to the above motivations %related to expressiveness, 
the limited style of higher-order communication enforced in \ahopi turns out to be interesting from a more pragmatic standpoint.
In fact, communication in \ahopi 
is inspired by those cases in which a process $P$
is communicated in a translated format $\encp{P}{}$,
and the translation is not compositional. That is, the cases in which, 
for any  process context $C$, 
the translation of $\ct{P}$ cannot be seen as a function of
the translation of $P$, i.e. 
%$\encp{ \ct{P}}{} \neq \encp{ C}{}[\encp{P}{}]$.
there exists no context $D$ such that
$\encp{ \ct{P}}{} = D[P]$.
This setting can be related to several existing programming scenarios. 
The simplest example is perhaps mobility based on already compiled code, 
on which it is not possible to
apply inverse translations (such as
reverse engineering).
Other examples include \emph{proof-carrying code} \cite{NeculaL98}
and communication of \emph{obfuscated code} \cite{CollbergT02}.
The former features communication of executable code that comes with a certificate: 
a recipient can only check the certificate and decide whether to execute the code or not.
The latter consists in the communication of 
source code that is made difficult to understand for, e.g., security/copyright reasons, while preserving its functionality.



The main contribution of the paper is the study of the expressiveness and decidability of termination and convergence in \ahopi.
Our main results are:
\begin{enumerate}
\item Similarly as \hocore, \ahopi is Turing complete. Therefore, despite the limitation of forward capabilities motivated above, the calculus has a significant expressive power. 
The result is obtained by exhibiting an encoding of Minsky machines.

\item In sharp contrast with \hocore, termination in \ahopi is \emph{decidable}. 
This result is obtained by appealing to the theory of well-structured transition systems (WSTS) \cite{FinkelS01}, following the approach used in \cite{Busi09}.
\end{enumerate}

As for (1) it is worth commenting that the encoding is not \emph{faithful}
in the sense that, unlike the encoding of
Minsky machines in \hocore, it may introduce computations which do not correspond to the expected
behavior of the modeled machine. Such computations are forced to be infinite and
thus regarded as non-halting computations which are therefore ignored. Only the finite
computations correspond to those of the encoded Minsky machine.
This way, we prove that the Minsky machines terminates iff its encoding in \ahopi converges. Consequently, convergence in \ahopi is undecidable.


As for (2), although using the theory of WSTS is certainly not a new approach, to the best of our knowledge this is the first time it is applied in the higher-order setting. This is significant because
the adaptation to the \ahopi case is far from trivial. Indeed, as we shall discuss, 
this approach %based on WSTS 
relies on over-approximating %a bound on the (set of) derivatives of a process.
%CORREGGERE 
an upper bound on the depth of the
(set of) derivatives of a process.
By \emph{depth} of a process we mean its
maximal nesting of input/output
actions.
Notice that, even with the limitation on forwarding enforced by \ahopi, because of the ``term copying'' feature of higher-order calculi, 
variable instantiation %of a variable with a process
might lead to a potentially larger process. 
Hence, finding suitable ways of bounding 
the set of derivatives of a process is rather challenging and needs care. 


\paragraph{Structure of the paper.} 
The syntax and semantics of \ahopi are introduced in Section \ref{s:lang}.
The encoding of Minsky machines into \ahopi, and the undecidability of convergence are discussed in
Section \ref{s:turing}. The decidability of termination is addressed in Section \ref{s:wsts}.
Some final remarks, as well as a review of related work, are included in Section \ref{s:conc}.